package com.googlecode.kipler.syntax.formula;

import com.googlecode.kipler.syntax.LTLBinaryOperator;

public class LTLBinaryFormula extends Formula {

	private LTLBinaryOperator constructor;

	private Formula lhs, rhs;

	public LTLBinaryFormula() {

	}

	public LTLBinaryFormula(LTLBinaryOperator constructor, Formula lhs, Formula rhs) {
		super();
		this.constructor = constructor;
		this.lhs = lhs;
		this.rhs = rhs;
	}

	public LTLBinaryOperator getConstructor() {
		return constructor;
	}

	public Formula getLhs() {
		return lhs;
	}

	public void setLhs(Formula lhs) {
		this.lhs = lhs;
	}

	public Formula getRhs() {
		return rhs;
	}

	public void setRhs(Formula rhs) {
		this.rhs = rhs;
	}

	public void setConstructor(LTLBinaryOperator constructor) {
		this.constructor = constructor;
	}

	@Override
	public boolean isNegated() {
		return false;
	}

	@Override
	public Formula toggleNegated() {
		if (getConstructor().equals(LTLBinaryOperator.UNTIL)) {
			setConstructor(LTLBinaryOperator.BEFORE);
		} else {
			setConstructor(LTLBinaryOperator.UNTIL);
		}
		setLhs(getLhs().toggleNegated());
		// rhs remains the same
		return this;
	}

	@Override
	public boolean equals(Object obj) {
		if (obj != null && (obj.getClass().equals(this.getClass()))) {
			LTLBinaryFormula other = (LTLBinaryFormula) obj;
			return (this.getConstructor().equals(other.getConstructor())
					&& this.getLhs().equals(other.getLhs()) && this.getRhs()
					.equals(other.getRhs()));
		}
		return false;
	}

	@Override
	public int hashCode() {
		return 17 * 37 + super.hashCode() + getConstructor().hashCode()
				+ getLhs().hashCode() + getRhs().hashCode();
	}

	public LTLBinaryFormula copy() {
		LTLBinaryFormula result = new LTLBinaryFormula();
		result.setConstructor(getConstructor());
		result.setLhs(getLhs().copy());
		result.setRhs(getRhs().copy());
		return result;
	}

	/**
	 * @see java.lang.Object#toString()
	 */
	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		buffer.append("(");
		buffer.append(getLhs());
		if (getConstructor() == LTLBinaryOperator.UNTIL)
			buffer.append(" U ");
		else
			buffer.append(" B ");
		buffer.append(getRhs());
		buffer.append(")");
		return buffer.toString();
	}

	@Override
	public void accept(FormulaVisitor v) {
		v.visitLTLBinaryFormula(this);
	}

}
